<HTML><HEAD>
<META NAME="description" CONTENT="Sets whose items may be compared according to a total order relation; implemented as sorted two-way lists.">
<META NAME="names" CONTENT="sorted_set, set, two_way_list">
<META NAME="legal" CONTENT="See notice at end of class.">
<META NAME="contents" CONTENT="generic">
<META NAME="access" CONTENT="membership, min, max">
<META NAME="representation" CONTENT="linked">
<META NAME="keywords" CONTENT="Eiffel class">
<META NAME="license" CONTENT="Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)">
<META NAME="copyright" CONTENT="Copyright (c) 1984-2008, Eiffel Software and others">
<META NAME="source" CONTENT="Eiffel Software 356 Storke Road, Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com">
<META NAME="library" CONTENT="EiffelBase: Library of reusable components for Eiffel.">
<META NAME="keywords" CONTENT="Eiffel class">
<TITLE>two_way_sorted_set Flat contracts</TITLE></HEAD>
<BODY BGCOLOR="white">
<P ALIGN="CENTER">Automatic generation produced by ISE Eiffel</P>
<PRE><TABLE BORDER="1" ALIGN="CENTER"><TR><TD><A HREF="../class_list.html">Classes</A></TD><TD><A HREF="../cluster_list.html">Clusters</A></TD><TD><A HREF="../cluster_hierarchy.html">Cluster hierarchy</A></TD><TD><A HREF="two_way_sorted_set_chart.html">Chart</A></TD><TD><A HREF="two_way_sorted_set_links.html">Relations</A></TD><TD>Flat contracts</TD></TR></TABLE><B>indexing</B>
    description: "[
        Sets whose items may be compared according to a total order relation;
        implemented as sorted two-way lists.
    ]"
    legal: "See notice at end of class."
    status: "See notice at end of class."
    names: sorted_set, set, two_way_list
    representation: linked
    access: membership, min, max
    contents: generic
    date: "$Date: 2008-05-24 02:24:07 +0200 (Sat, 24 May 2008) $"
    revision: "$Revision: 170 $"

<B>class</B> <B>interface</B>
    <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G -&gt; <A HREF="../base/comparable_flatshort.html">COMPARABLE</A>]


<B>create</B> 
    <A NAME="f_make"><A HREF="../base/linked_list_flatshort.html#f_make">make</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create an empty list.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
            is_before: <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
</A>

<B>create</B> {<A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A>}
    <A NAME="f_make_sublist"><A HREF="../base/two_way_list_flatshort.html#f_make_sublist">make_sublist</A> (first_item, last_item: <B>like</B> <A HREF="../base/two_way_list_flatshort.html#f_first_element">first_element</A>; n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create sublist</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
</A>
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access</FONT>

    <A NAME="f_cursor"><A HREF="../base/two_way_list_flatshort.html#f_cursor">cursor</A>: <A HREF="../base/two_way_list_cursor_flatshort.html">TWO_WAY_LIST_CURSOR</A> [G]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Current cursor position</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/cursor_structure_flatshort.html">CURSOR_STRUCTURE</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/cursor_structure_flatshort.html">CURSOR_STRUCTURE</A>
            cursor_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_first"><A HREF="../base/linked_list_flatshort.html#f_first">first</A>: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Item at first position</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_first_element"><A HREF="../base/two_way_list_flatshort.html#f_first_element">first_element</A>: ?<B>like</B> <A HREF="../base/two_way_list_flatshort.html#f_new_cell">new_cell</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Head of list</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Anchor redefinition)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_generating_type"><A HREF="../base/any_flatshort.html#f_generating_type">generating_type</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Name of current object's generating type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (type of which it is a direct instance)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            generating_type_not_void: <B>Result</B> /= <B>Void</B>
            generating_type_not_empty: <B>not</B> <B>Result</B>.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_generator"><A HREF="../base/any_flatshort.html#f_generator">generator</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Name of current object's generating class</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (base class of the type of which it is a direct instance)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            generator_not_void: <B>Result</B> /= <B>Void</B>
            generator_not_empty: <B>not</B> <B>Result</B>.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_has"><A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v: G): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does structure include </FONT>`v'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Reference or object equality,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> based on </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/part_sorted_list_flatshort.html">PART_SORTED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/container_flatshort.html">CONTAINER</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            not_found_in_empty: <B>Result</B> <B>implies</B> <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_i_th"><B>i_th</B> <B>alias</B> "[]" (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A> <B>assign</B> <A HREF="../base/chain_flatshort.html#f_put_i_th">put_i_th</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Item at </FONT>`i'<FONT COLOR="red">-th position</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red"> as synonym of </FONT><B>infix</B> "@"<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/table_flatshort.html">TABLE</A>
            valid_key: <A HREF="../base/chain_flatshort.html#f_valid_index">valid_index</A> (i)
</A>
    <A NAME="f_index"><A HREF="../base/linked_list_flatshort.html#f_index">index</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Index of current position</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_flatshort.html">LINEAR</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            <B>True</B>
</A>
    <A NAME="f_index_of"><A HREF="../base/chain_flatshort.html#f_index_of">index_of</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>; i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Index of </FONT>`i'<FONT COLOR="red">-th occurrence of item identical to </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Reference or object equality,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> based on </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if none.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            positive_occurrences: i &gt; 0
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            non_negative_result: <B>Result</B> &gt;= 0
</A>
    <A NAME="f_item"><A HREF="../base/linked_list_flatshort.html#f_item">item</A>: G
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Current item</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            not_off: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/active_flatshort.html">ACTIVE</A>
            readable: <A HREF="../base/linked_list_flatshort.html#f_readable">readable</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A>
            not_off: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>
</A>
    <A NAME="f_item_for_iteration"><A HREF="../base/linear_flatshort.html#f_item_for_iteration">item_for_iteration</A>: G
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Item at current position</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            not_off: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>
</A>
    <A NAME="f_last"><A HREF="../base/linked_list_flatshort.html#f_last">last</A>: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Item at last position</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_last_element"><A HREF="../base/two_way_list_flatshort.html#f_last_element">last_element</A>: <B>like</B> <A HREF="../base/two_way_list_flatshort.html#f_first_element">first_element</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Tail of the list</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_occurrences"><A HREF="../base/linear_flatshort.html#f_occurrences">sequential_occurrences</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of times </FONT>`v'<FONT COLOR="red"> appears.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Reference or object equality,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> based on </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/bag_flatshort.html">BAG</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bag_flatshort.html">BAG</A>
            non_negative_occurrences: <B>Result</B> &gt;= 0
</A>
    <A NAME="f_search_after"><A HREF="../base/part_sorted_list_flatshort.html#f_search_after">search_after</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Go to first position with item greater</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> than or equal to </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/part_sorted_list_flatshort.html">PART_SORTED_LIST</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/part_sorted_list_flatshort.html">PART_SORTED_LIST</A>
            argument_less_than_item: (<B>not</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>) <B>implies</B> (v &lt;= <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
</A>
    <A NAME="f_search_before"><A HREF="../base/part_sorted_list_flatshort.html#f_search_before">search_before</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Go to last position with item less</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> than or equal to </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/part_sorted_list_flatshort.html">PART_SORTED_LIST</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/part_sorted_list_flatshort.html">PART_SORTED_LIST</A>
            (<B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_item">item</A> &lt;= v)
</A>
    <A NAME="f_sublist"><A HREF="../base/two_way_list_flatshort.html#f_sublist">sublist</A>: ?<A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Result produced by last </FONT><A HREF="../base/two_way_list_flatshort.html#f_split">split</A>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_infix "@""><B>infix</B> "@" (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A> <B>assign</B> <A HREF="../base/chain_flatshort.html#f_put_i_th">put_i_th</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Item at </FONT>`i'<FONT COLOR="red">-th position</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/chain_flatshort.html#f_i_th">i_th</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/table_flatshort.html">TABLE</A>
            valid_key: <A HREF="../base/chain_flatshort.html#f_valid_index">valid_index</A> (i)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Measurement</FONT>

    <A NAME="f_count"><A HREF="../base/linked_list_flatshort.html#f_count">count</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of items</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_index_set"><A HREF="../base/chain_flatshort.html#f_index_set">index_set</A>: <A HREF="../base/integer_interval_flatshort.html">INTEGER_INTERVAL</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Range of acceptable indexes</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            not_void: <B>Result</B> /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            count_definition: <B>Result</B>.<A HREF="../base/integer_interval_flatshort.html#f_count">count</A> = <A HREF="../base/linked_list_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_max"><A HREF="../base/sorted_list_flatshort.html#f_max">max</A>: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Maximum item</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_set_flatshort.html">COMPARABLE_SET</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A>
            max_is_last: <B>Result</B> = <A HREF="../base/linked_list_flatshort.html#f_last">last</A>
</A>
    <A NAME="f_median"><A HREF="../base/sorted_list_flatshort.html#f_median">median</A>: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Median item</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A>
            median_definition: <B>Result</B> = <A HREF="../base/chain_flatshort.html#f_i_th">i_th</A> ((<A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1) // 2)
</A>
    <A NAME="f_min"><A HREF="../base/sorted_list_flatshort.html#f_min">min</A>: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Minimum item</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_set_flatshort.html">COMPARABLE_SET</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A>
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sorted_list_flatshort.html">SORTED_LIST</A>
            min_is_first: <B>Result</B> = <A HREF="../base/linked_list_flatshort.html#f_first">first</A>
</A>
    <A NAME="f_occurrences"><A HREF="../base/chain_flatshort.html#f_occurrences">occurrences</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of times </FONT>`v'<FONT COLOR="red"> appears.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Reference or object equality,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> based on </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/bag_flatshort.html">BAG</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_flatshort.html">LINEAR</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bag_flatshort.html">BAG</A>
            non_negative_occurrences: <B>Result</B> &gt;= 0
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Comparison</FONT>

    <A NAME="f_deep_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> or attached to isomorphic object structures?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            shallow_implies_deep: <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (some, other) <B>implies</B> <B>Result</B>
            both_or_none_void: (some = <B>Void</B>) <B>implies</B> (<B>Result</B> = (other = <B>Void</B>))
            same_type: (<B>Result</B> <B>and</B> (some /= <B>Void</B>)) <B>implies</B> (other /= <B>Void</B> <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other))
            symmetric: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (other, some)
</A>
    <A NAME="f_disjoint"><A HREF="../base/traversable_subset_flatshort.html#f_disjoint">disjoint</A> (other: <A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A> [G]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do current set and </FONT>`other'<FONT COLOR="red"> have no</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> items in common?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>
    <A NAME="f_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_equal">equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void or attached</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to objects considered equal?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (some = <B>Void</B> <B>and</B> other = <B>Void</B>) <B>or else</B> ((some /= <B>Void</B> <B>and</B> other /= <B>Void</B>) <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (other))
</A>
    <A NAME="f_is_deep_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_is_deep_equal">is_deep_equal</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`Current'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> attached to isomorphic object structures?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            shallow_implies_deep: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
            same_type: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_is_deep_equal">is_deep_equal</A> (<B>Current</B>)
</A>
    <A NAME="f_is_equal"><A HREF="../base/list_flatshort.html#f_is_equal">is_equal</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`other'<FONT COLOR="red"> contain the same elements?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/list_flatshort.html">LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
            consistent: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/list_flatshort.html">LIST</A>
            indices_unchanged: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> <B>and</B> other.<A HREF="../base/linear_flatshort.html#f_index">index</A> = <B>old</B> other.<A HREF="../base/linear_flatshort.html#f_index">index</A>
            true_implies_same_size: <B>Result</B> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = other.<A HREF="../base/finite_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_is_subset"><A HREF="../base/traversable_subset_flatshort.html#f_is_subset">is_subset</A> (other: <A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A> [G]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current set a subset of </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>
    <A NAME="f_is_superset"><A HREF="../base/subset_flatshort.html#f_is_superset">is_superset</A> (other: <A HREF="../base/subset_flatshort.html">SUBSET</A> [G]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current set a superset of </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>
    <A NAME="f_standard_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void or attached to</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> field-by-field identical objects of the same type?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Always uses default object comparison criterion.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (some = <B>Void</B> <B>and</B> other = <B>Void</B>) <B>or else</B> ((some /= <B>Void</B> <B>and</B> other /= <B>Void</B>) <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other))
</A>
    <A NAME="f_standard_is_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`other'<FONT COLOR="red"> attached to an object of the same type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> as current object, and field-by-field identical to it?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            same_type: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (<B>Current</B>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Status report</FONT>

    <A NAME="f_after"><A HREF="../base/linked_list_flatshort.html#f_after">after</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is there no valid cursor position to the right of cursor?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_before"><A HREF="../base/linked_list_flatshort.html#f_before">before</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is there no valid cursor position to the left of cursor?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_conforms_to"><A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (other: <A HREF="../base/any_flatshort.html">ANY</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does type of current object conform to type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of </FONT>`other'<FONT COLOR="red"> (as per Eiffel: The Language, chapter 13)?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
</A>
    <A NAME="f_exhausted"><A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Has structure been completely explored?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            exhausted_when_off: <A HREF="../base/linked_list_flatshort.html#f_off">off</A> <B>implies</B> <B>Result</B>
</A>
    <A NAME="f_extendible"><A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>True</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May new items be added? (Answer: yes.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A><FONT COLOR="red">)</FONT>

    <A NAME="f_full"><A HREF="../base/linked_list_flatshort.html#f_full">full</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>False</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is structured filled to capacity? (Answer: no.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>

    <A NAME="f_is_empty"><A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is structure empty?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/finite_flatshort.html">FINITE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/container_flatshort.html">CONTAINER</A>
            <B>True</B>
</A>
    <A NAME="f_is_inserted"><A HREF="../base/collection_flatshort.html#f_is_inserted">is_inserted</A> (v: G): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Has </FONT>`v'<FONT COLOR="red"> been inserted by the most recent insertion?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (By default, the value returned is equivalent to calling </FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT>`has (v)'<FONT COLOR="red">. However, descendants might be able to provide more</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> efficient implementations.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_isfirst"><A HREF="../base/linked_list_flatshort.html#f_isfirst">isfirst</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is cursor at first position?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/chain_flatshort.html">CHAIN</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            valid_position: <B>Result</B> <B>implies</B> <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_islast"><A HREF="../base/two_way_list_flatshort.html#f_islast">islast</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is cursor at last position?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/chain_flatshort.html">CHAIN</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            valid_position: <B>Result</B> <B>implies</B> <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_object_comparison"><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Must search operations use </FONT><A HREF="../base/any_flatshort.html#f_equal">equal</A><FONT COLOR="red"> rather than </FONT>`='
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> for comparing references? (Default: no, use </FONT>`='<FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A><FONT COLOR="red">)</FONT>

    <A NAME="f_off"><A HREF="../base/linked_list_flatshort.html#f_off">off</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is there no current item?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A>
            <B>True</B>
</A>
    <A NAME="f_prunable"><A HREF="../base/dynamic_chain_flatshort.html#f_prunable">prunable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May items be removed? (Answer: yes.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/collection_flatshort.html">COLLECTION</A>
            <B>True</B>
</A>
    <A NAME="f_readable"><A HREF="../base/linked_list_flatshort.html#f_readable">readable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is there a current item that may be read?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/active_flatshort.html">ACTIVE</A>
            <B>True</B>
</A>
    <A NAME="f_same_type"><A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other: <A HREF="../base/any_flatshort.html">ANY</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is type of current object identical to type of </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (<A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (other) <B>and</B> other.<A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (<B>Current</B>))
</A>
    <A NAME="f_sorted"><A HREF="../base/sorted_two_way_list_flatshort.html#f_sorted">sorted</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is the structure sorted?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sorted_two_way_list_flatshort.html">SORTED_TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_valid_cursor"><A HREF="../base/linked_list_flatshort.html#f_valid_cursor">valid_cursor</A> (p: <A HREF="../base/cursor_flatshort.html">CURSOR</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Can the cursor be moved to position </FONT>`p'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/cursor_structure_flatshort.html">CURSOR_STRUCTURE</A>
            <B>True</B>
</A>
    <A NAME="f_valid_cursor_index"><A HREF="../base/chain_flatshort.html#f_valid_cursor_index">valid_cursor_index</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`i'<FONT COLOR="red"> correctly bounded for cursor movement?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            valid_cursor_index_definition: <B>Result</B> = ((i &gt;= 0) <B>and</B> (i &lt;= <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1))
</A>
    <A NAME="f_valid_index"><A HREF="../base/chain_flatshort.html#f_valid_index">valid_index</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`i'<FONT COLOR="red"> within allowable bounds?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/table_flatshort.html">TABLE</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            <B>True</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            only_if_in_index_set: <B>Result</B> <B>implies</B> ((i &gt;= <A HREF="../base/chain_flatshort.html#f_index_set">index_set</A>.<A HREF="../base/integer_interval_flatshort.html#f_lower">lower</A>) <B>and</B> (i &lt;= <A HREF="../base/chain_flatshort.html#f_index_set">index_set</A>.<A HREF="../base/integer_interval_flatshort.html#f_upper">upper</A>))
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            index_valid: 0 &lt;= i <B>and</B> i &lt;= <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            valid_index_definition: <B>Result</B> = ((i &gt;= 1) <B>and</B> (i &lt;= <A HREF="../base/linked_list_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_writable"><A HREF="../base/sequence_flatshort.html#f_writable">writable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is there a current item that may be modified?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sequence_flatshort.html">SEQUENCE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/active_flatshort.html">ACTIVE</A>
            <B>True</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Status setting</FONT>

    <A NAME="f_compare_objects"><A HREF="../base/container_flatshort.html#f_compare_objects">compare_objects</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that future search operations will use </FONT><A HREF="../base/any_flatshort.html#f_equal">equal</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> rather than </FONT>`='<FONT COLOR="red"> for comparing references.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            changeable_comparison_criterion: <A HREF="../base/set_flatshort.html#f_changeable_comparison_criterion">changeable_comparison_criterion</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>
    <A NAME="f_compare_references"><A HREF="../base/container_flatshort.html#f_compare_references">compare_references</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that future search operations will use </FONT>`='
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> rather than </FONT><A HREF="../base/any_flatshort.html#f_equal">equal</A><FONT COLOR="red"> for comparing references.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            changeable_comparison_criterion: <A HREF="../base/set_flatshort.html#f_changeable_comparison_criterion">changeable_comparison_criterion</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            reference_comparison: <B>not</B> <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Cursor movement</FONT>

    <A NAME="f_back"><A HREF="../base/two_way_list_flatshort.html#f_back">back</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to previous position, if any.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bilinear_flatshort.html">BILINEAR</A>
            not_before: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
</A>
    <A NAME="f_finish"><A HREF="../base/two_way_list_flatshort.html#f_finish">finish</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to last position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Go before if empty)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_flatshort.html">LINEAR</A>
            <B>True</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            at_last: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <A HREF="../base/two_way_list_flatshort.html#f_islast">islast</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
            empty_convention: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A>
            not_after: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
</A>
    <A NAME="f_forth"><A HREF="../base/two_way_list_flatshort.html#f_forth">forth</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to next position, if any.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            not_after: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A>
            not_after: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/list_flatshort.html">LIST</A>
            moved_forth: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + 1
</A>
    <A NAME="f_go_i_th"><A HREF="../base/linked_list_flatshort.html#f_go_i_th">go_i_th</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to </FONT>`i'<FONT COLOR="red">-th position.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            valid_cursor_index: <A HREF="../base/chain_flatshort.html#f_valid_cursor_index">valid_cursor_index</A> (i)
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            valid_index: <A HREF="../base/chain_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            position_expected: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = i
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            cursor_moved: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = i
</A>
    <A NAME="f_go_to"><A HREF="../base/linked_list_flatshort.html#f_go_to">go_to</A> (p: <A HREF="../base/cursor_flatshort.html">CURSOR</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to position </FONT>`p'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/cursor_structure_flatshort.html">CURSOR_STRUCTURE</A>
            cursor_position_valid: <A HREF="../base/linked_list_flatshort.html#f_valid_cursor">valid_cursor</A> (p)
</A>
    <A NAME="f_move"><A HREF="../base/two_way_list_flatshort.html#f_move">move</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor </FONT>`i'<FONT COLOR="red"> positions. The cursor</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> may end up </FONT><A HREF="../base/linked_list_flatshort.html#f_off">off</A><FONT COLOR="red"> if the offset is to big.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/chain_flatshort.html">CHAIN</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            too_far_right: (<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i &gt; <A HREF="../base/linked_list_flatshort.html#f_count">count</A>) <B>implies</B> <A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A>
            too_far_left: (<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i &lt; 1) <B>implies</B> <A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A>
            expected_index: (<B>not</B> <A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A>) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
            moved_if_inbounds: ((<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i) &gt;= 0 <B>and</B> (<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i) &lt;= (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1)) <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = (<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i)
            before_set: (<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i) &lt;= 0 <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
            after_set: (<B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + i) &gt;= (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1) <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
</A>
    <A NAME="f_search"><A HREF="../base/bilinear_flatshort.html#f_search">search</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move to first position (at or after current</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> position) where </FONT><A HREF="../base/linked_list_flatshort.html#f_item">item</A><FONT COLOR="red"> and </FONT>`v'<FONT COLOR="red"> are equal.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> If structure does not include </FONT>`v'<FONT COLOR="red"> ensure that</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT><A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A><FONT COLOR="red"> will be true.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Reference or object equality,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> based on </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/bilinear_flatshort.html">BILINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/linear_flatshort.html">LINEAR</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            object_found: (<B>not</B> <A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A> <B>and</B> <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>) <B>implies</B> <A HREF="../base/any_flatshort.html#f_equal">equal</A> (v, <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            item_found: (<B>not</B> <A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A> <B>and</B> <B>not</B> <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>) <B>implies</B> v = <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
</A>
    <A NAME="f_start"><A HREF="../base/linked_list_flatshort.html#f_start">start</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to first position.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A>
            <B>True</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            at_first: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_isfirst">isfirst</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
            empty_convention: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Element change</FONT>

    <A NAME="f_append"><A HREF="../base/chain_flatshort.html#f_append">append</A> (s: <A HREF="../base/sequence_flatshort.html">SEQUENCE</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append a copy of </FONT>`s'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sequence_flatshort.html">SEQUENCE</A>
            argument_not_void: s /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sequence_flatshort.html">SEQUENCE</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> &gt;= <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_extend"><A HREF="../base/two_way_sorted_set_flatshort.html#f_extend">extend</A> (v: G)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that structure includes </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/two_way_sorted_set_flatshort.html#f_put">put</A><FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            item_inserted: <A HREF="../base/collection_flatshort.html#f_is_inserted">is_inserted</A> (v)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/set_flatshort.html">SET</A>
            in_set_already: <B>old</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A>)
            added_to_set: <B>not</B> <B>old</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1)
</A>
    <A NAME="f_fill"><A HREF="../base/chain_flatshort.html#f_fill">fill</A> (other: <A HREF="../base/container_flatshort.html">CONTAINER</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Fill with as many items of </FONT>`other'<FONT COLOR="red"> as possible.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> The representations of </FONT>`other'<FONT COLOR="red"> and current structure</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> need not be the same.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            other_not_void: other /= <B>Void</B>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
</A>
    <A NAME="f_force"><A HREF="../base/sequence_flatshort.html#f_force">force</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add </FONT>`v'<FONT COLOR="red"> to end.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sequence_flatshort.html">SEQUENCE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sequence_flatshort.html">SEQUENCE</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/sequence_flatshort.html">SEQUENCE</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1
            item_inserted: <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v)
</A>
    <A NAME="f_merge"><A HREF="../base/two_way_sorted_set_flatshort.html#f_merge">merge</A> (other: <A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add all items of </FONT>`other'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>
    <A NAME="f_merge_left"><A HREF="../base/two_way_list_flatshort.html#f_merge_left">merge_left</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Merge </FONT>`other'<FONT COLOR="red"> into current structure before cursor</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> position. Do not move cursor. Empty </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
            not_before: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
            other_exists: other /= <B>Void</B>
            not_current: other /= <B>Current</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + <B>old</B> other.<A HREF="../base/finite_flatshort.html#f_count">count</A>
            new_index: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + <B>old</B> other.<A HREF="../base/finite_flatshort.html#f_count">count</A>
            other_is_empty: other.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_merge_right"><A HREF="../base/two_way_list_flatshort.html#f_merge_right">merge_right</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Merge </FONT>`other'<FONT COLOR="red"> into current structure after cursor</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> position. Do not move cursor. Empty </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
            not_after: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
            other_exists: other /= <B>Void</B>
            not_current: other /= <B>Current</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + <B>old</B> other.<A HREF="../base/finite_flatshort.html#f_count">count</A>
            same_index: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A>
            other_is_empty: other.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_move_item"><A HREF="../base/linear_subset_flatshort.html#f_move_item">move_item</A> (v: G)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move </FONT>`v'<FONT COLOR="red"> to the left of cursor.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            item_exists: v /= <B>Void</B>
            item_in_set: <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v)
</A>
    <A NAME="f_put"><A HREF="../base/two_way_sorted_set_flatshort.html#f_put">put</A> (v: G)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that structure includes </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/two_way_sorted_set_flatshort.html#f_extend">extend</A><FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            item_inserted: <A HREF="../base/collection_flatshort.html#f_is_inserted">is_inserted</A> (v)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/set_flatshort.html">SET</A>
            in_set_already: <B>old</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A>)
            added_to_set: <B>not</B> <B>old</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1)
</A>
    <A NAME="f_put_front"><A HREF="../base/two_way_list_flatshort.html#f_put_front">put_front</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add </FONT>`v'<FONT COLOR="red"> to beginning.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do not move cursor.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1
            item_inserted: <A HREF="../base/linked_list_flatshort.html#f_first">first</A> = v
</A>
    <A NAME="f_put_i_th"><A HREF="../base/chain_flatshort.html#f_put_i_th">put_i_th</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>; i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Put </FONT>`v'<FONT COLOR="red"> at </FONT>`i'<FONT COLOR="red">-th position.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/table_flatshort.html">TABLE</A>
            valid_key: <A HREF="../base/chain_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            insertion_done: <A HREF="../base/chain_flatshort.html#f_i_th">i_th</A> (i) = v
</A>
    <A NAME="f_put_left"><A HREF="../base/two_way_list_flatshort.html#f_put_left">put_left</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add </FONT>`v'<FONT COLOR="red"> to the left of cursor position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do not move cursor.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
            not_before: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            item_exists: v /= <B>Void</B>
            not_before: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1
            new_index: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> + 1
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
            previous_exists: <A HREF="../base/two_way_list_flatshort.html#f_previous">previous</A> /= <B>Void</B>
            item_inserted: {q: <B>like</B> <A HREF="../base/two_way_list_flatshort.html#f_previous">previous</A>} <A HREF="../base/two_way_list_flatshort.html#f_previous">previous</A> and then q.item = v
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
            cursor_position_unchanged: index = <B>old</B> index + 1
</A>
    <A NAME="f_put_right"><A HREF="../base/two_way_list_flatshort.html#f_put_right">put_right</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add </FONT>`v'<FONT COLOR="red"> to the right of cursor position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do not move cursor.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            extendible: <A HREF="../base/dynamic_chain_flatshort.html#f_extendible">extendible</A>
            not_after: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> + 1
            same_index: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
            next_exists: <A HREF="../base/linked_list_flatshort.html#f_next">next</A> /= <B>Void</B>
            item_inserted: <B>not</B> <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A> implies ({n: <B>like</B> next} next and then n.item = v)
            item_inserted_before: <B>old</B> before implies ({c: <B>like</B> active} active and then c.item = v)
</A>
    <A NAME="f_replace"><A HREF="../base/linked_list_flatshort.html#f_replace">replace</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace current item by </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/active_flatshort.html">ACTIVE</A>
            writable: <A HREF="../base/sequence_flatshort.html#f_writable">writable</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/active_flatshort.html">ACTIVE</A>
            item_replaced: <A HREF="../base/linked_list_flatshort.html#f_item">item</A> = v
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Removal</FONT>

    <A NAME="f_changeable_comparison_criterion"><A HREF="../base/set_flatshort.html#f_changeable_comparison_criterion">changeable_comparison_criterion</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red"> be changed?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Answer: only if set empty; otherwise insertions might</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> introduce duplicates, destroying the set property.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/set_flatshort.html">SET</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/container_flatshort.html">CONTAINER</A>
            <B>True</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/set_flatshort.html">SET</A>
            only_on_empty: <B>Result</B> = <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_prune"><A HREF="../base/two_way_sorted_set_flatshort.html#f_prune">prune</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove </FONT>`v'<FONT COLOR="red"> if present.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            prunable: <A HREF="../base/dynamic_chain_flatshort.html#f_prunable">prunable</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/set_flatshort.html">SET</A>
            removed_count_change: <B>old</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> - 1)
            not_removed_no_count_change: <B>not</B> <B>old</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v) <B>implies</B> (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A>)
            item_deleted: <B>not</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v)
</A>
    <A NAME="f_prune_all"><A HREF="../base/sorted_two_way_list_flatshort.html#f_prune_all">prune_all</A> (v: <B>like</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all items identical to </FONT>`v'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Reference or object equality,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> based on </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Leave cursor </FONT><A HREF="../base/linked_list_flatshort.html#f_off">off</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sorted_two_way_list_flatshort.html">SORTED_TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            prunable: <A HREF="../base/dynamic_chain_flatshort.html#f_prunable">prunable</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            no_more_occurrences: <B>not</B> <A HREF="../base/part_sorted_list_flatshort.html#f_has">has</A> (v)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            is_exhausted: <A HREF="../base/linear_flatshort.html#f_exhausted">exhausted</A>
</A>
    <A NAME="f_remove"><A HREF="../base/two_way_list_flatshort.html#f_remove">remove</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove current item.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor to right neighbor</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (or </FONT><A HREF="../base/linked_list_flatshort.html#f_after">after</A><FONT COLOR="red"> if no right neighbor).</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/active_flatshort.html">ACTIVE</A>
            prunable: <A HREF="../base/dynamic_chain_flatshort.html#f_prunable">prunable</A>
            writable: <A HREF="../base/sequence_flatshort.html#f_writable">writable</A>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A>
            not_off: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_list_flatshort.html">DYNAMIC_LIST</A>
            after_when_empty: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
</A>
    <A NAME="f_remove_left"><A HREF="../base/two_way_list_flatshort.html#f_remove_left">remove_left</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove item to the left of cursor position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do not move cursor.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            left_exists: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> &gt; 1
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> - 1
            new_index: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A> - 1
</A>
    <A NAME="f_remove_right"><A HREF="../base/two_way_list_flatshort.html#f_remove_right">remove_right</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove item to the right of cursor position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do not move cursor.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            right_exists: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> &lt; <A HREF="../base/linked_list_flatshort.html#f_count">count</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
            new_count: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_count">count</A> - 1
            same_index: <A HREF="../base/linked_list_flatshort.html#f_index">index</A> = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_index">index</A>
</A>
    <A NAME="f_remove_sublist"><A HREF="../base/two_way_list_flatshort.html#f_remove_sublist">remove_sublist</A>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_split"><A HREF="../base/two_way_list_flatshort.html#f_split">split</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove from current list</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> min (</FONT>`n'<FONT COLOR="red">, </FONT><A HREF="../base/linked_list_flatshort.html#f_count">count</A><FONT COLOR="red"> - </FONT><A HREF="../base/linked_list_flatshort.html#f_index">index</A><FONT COLOR="red"> - 1) items</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> starting at cursor position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Move cursor right one position.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Make extracted sublist accessible</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> through attribute </FONT><A HREF="../base/two_way_list_flatshort.html#f_sublist">sublist</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A>
            not_off: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>
            valid_sublist: n &gt;= 0
</A>
    <A NAME="f_wipe_out"><A HREF="../base/two_way_list_flatshort.html#f_wipe_out">wipe_out</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all items.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            prunable: <A HREF="../base/dynamic_chain_flatshort.html#f_prunable">prunable</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            wiped_out: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_list_flatshort.html">DYNAMIC_LIST</A>
            is_before: <A HREF="../base/linked_list_flatshort.html#f_before">before</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Transformation</FONT>

    <A NAME="f_sort"><A HREF="../base/sorted_two_way_list_flatshort.html#f_sort">sort</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Sort all items.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Has O(</FONT><A HREF="../base/linked_list_flatshort.html#f_count">count</A><FONT COLOR="red"> * log (</FONT><A HREF="../base/linked_list_flatshort.html#f_count">count</A><FONT COLOR="red">)) complexity.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/sorted_two_way_list_flatshort.html">SORTED_TWO_WAY_LIST</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_swap"><A HREF="../base/chain_flatshort.html#f_swap">swap</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Exchange item at </FONT>`i'<FONT COLOR="red">-th position with item</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> at cursor position.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            not_off: <B>not</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>
            valid_index: <A HREF="../base/chain_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            swapped_to_item: <A HREF="../base/linked_list_flatshort.html#f_item">item</A> = <B>old</B> <A HREF="../base/chain_flatshort.html#f_i_th">i_th</A> (i)
            swapped_from_item: <A HREF="../base/chain_flatshort.html#f_i_th">i_th</A> (i) = <B>old</B> <A HREF="../base/linked_list_flatshort.html#f_item">item</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Conversion</FONT>

    <A NAME="f_linear_representation"><A HREF="../base/linear_flatshort.html#f_linear_representation">linear_representation</A>: <A HREF="../base/linear_flatshort.html">LINEAR</A> [G]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Representation as a linear structure</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/container_flatshort.html">CONTAINER</A>
            <B>True</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Duplication</FONT>

    <A NAME="f_copy"><A HREF="../base/any_flatshort.html#f_copy">copy</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Update current object using fields of object attached</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to </FONT>`other'<FONT COLOR="red">, so as to yield equal objects.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
            type_identity: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            is_equal: <A HREF="../base/list_flatshort.html#f_is_equal">is_equal</A> (other)
</A>
    <A NAME="f_deep_copy"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_copy">deep_copy</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Effect equivalent to that of:</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red">		</FONT><A HREF="../base/any_flatshort.html#f_copy">copy</A><FONT COLOR="red"> (</FONT>`other'<FONT COLOR="red"> . </FONT><A HREF="../base/any_flatshort.html#f_deep_twin">deep_twin</A><FONT COLOR="red">)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            deep_equal: <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (<B>Current</B>, other)
</A>
    <A NAME="f_deep_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_twin">deep_twin</A>: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object structure recursively duplicated from Current.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            deep_twin_not_void: <B>Result</B> /= <B>Void</B>
            deep_equal: <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (<B>Current</B>, <B>Result</B>)
</A>
    <A NAME="f_duplicate"><A HREF="../base/two_way_sorted_set_flatshort.html#f_duplicate">duplicate</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy of sub-set beginning at cursor position</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> and having min (</FONT>`n'<FONT COLOR="red">, </FONT><A HREF="../base/linked_list_flatshort.html#f_count">count</A><FONT COLOR="red"> - </FONT><A HREF="../base/linked_list_flatshort.html#f_index">index</A><FONT COLOR="red"> + 1) items</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
            not_off_unless_after: <A HREF="../base/linked_list_flatshort.html#f_off">off</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_after">after</A>
            valid_subchain: n &gt;= 0
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            non_negative: n &gt;= 0
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            correct_count_1: n &lt;= <A HREF="../base/linked_list_flatshort.html#f_count">count</A> <B>implies</B> <B>Result</B>.<A HREF="../base/set_flatshort.html#f_count">count</A> = n
            correct_count_2: n &gt;= <A HREF="../base/linked_list_flatshort.html#f_count">count</A> <B>implies</B> <B>Result</B>.<A HREF="../base/set_flatshort.html#f_count">count</A> = <A HREF="../base/linked_list_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_standard_copy"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_copy">standard_copy</A> (other: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy every field of </FONT>`other'<FONT COLOR="red"> onto corresponding field</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
            type_identity: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            is_standard_equal: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other)
</A>
    <A NAME="f_standard_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_twin">standard_twin</A>: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object field-by-field identical to </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Always uses default copying semantics.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            standard_twin_not_void: <B>Result</B> /= <B>Void</B>
            equal: <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (<B>Result</B>, <B>Current</B>)
</A>
    <A NAME="f_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>: <A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object equal to </FONT>`Current'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT><A HREF="../base/any_flatshort.html#f_twin">twin</A><FONT COLOR="red"> calls </FONT><A HREF="../base/any_flatshort.html#f_copy">copy</A><FONT COLOR="red">; to change copying/twining semantics, redefine </FONT><A HREF="../base/any_flatshort.html#f_copy">copy</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            twin_not_void: <B>Result</B> /= <B>Void</B>
            is_equal: <B>Result</B>.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Basic operations</FONT>

    <A NAME="f_default"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_default">default</A>: ?<A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A> [G]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Default value of object's type</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_default_pointer"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>: <A HREF="../base/pointer_flatshort.html">POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Default value of type </FONT>`POINTER'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Avoid the need to write </FONT>`p'<FONT COLOR="red">.</FONT><A HREF="../base/any_flatshort.html#f_default">default</A><FONT COLOR="red"> for</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> some </FONT>`p'<FONT COLOR="red"> of type </FONT>`POINTER'<FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_default_rescue"><A HREF="../base/any_flatshort.html#f_default_rescue">default_rescue</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Process exception for routines with no Rescue clause.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Default: do nothing.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_do_nothing"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_do_nothing">do_nothing</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Execute a null action.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_intersect"><A HREF="../base/two_way_sorted_set_flatshort.html#f_intersect">intersect</A> (other: <B>like</B> <B>Current</B>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all items not in </FONT>`other'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            is_subset_other: <A HREF="../base/traversable_subset_flatshort.html#f_is_subset">is_subset</A> (other)
</A>
    <A NAME="f_subtract"><A HREF="../base/two_way_sorted_set_flatshort.html#f_subtract">subtract</A> (other: <B>like</B> <B>Current</B>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all items also in </FONT>`other'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            is_disjoint: <A HREF="../base/traversable_subset_flatshort.html#f_disjoint">disjoint</A> (other)
</A>
    <A NAME="f_symdif"><A HREF="../base/traversable_subset_flatshort.html#f_symdif">symdif</A> (other: <A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A> [G])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all items also in </FONT>`other'<FONT COLOR="red">, and add all</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> items of </FONT>`other'<FONT COLOR="red"> not already present.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/subset_flatshort.html">SUBSET</A>
            set_exists: other /= <B>Void</B>
            same_rule: <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A> = other.<A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Iteration</FONT>

    <A NAME="f_do_all"><A HREF="../base/linear_flatshort.html#f_do_all">do_all</A> (action: <A HREF="../base/procedure_flatshort.html">PROCEDURE</A> [<A HREF="../base/any_flatshort.html">ANY</A>, <A HREF="../base/tuple_flatshort.html">TUPLE</A> [G]])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Apply </FONT>`action'<FONT COLOR="red"> to every item.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Semantics not guaranteed if </FONT>`action'<FONT COLOR="red"> changes the structure;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> in such a case, apply iterator to clone of structure instead.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            action_exists: action /= <B>Void</B>
</A>
    <A NAME="f_do_if"><A HREF="../base/linear_flatshort.html#f_do_if">do_if</A> (action: <A HREF="../base/procedure_flatshort.html">PROCEDURE</A> [<A HREF="../base/any_flatshort.html">ANY</A>, <A HREF="../base/tuple_flatshort.html">TUPLE</A> [G]]; test: <A HREF="../base/function_flatshort.html">FUNCTION</A> [<A HREF="../base/any_flatshort.html">ANY</A>, <A HREF="../base/tuple_flatshort.html">TUPLE</A> [G], <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Apply </FONT>`action'<FONT COLOR="red"> to every item that satisfies </FONT>`test'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Semantics not guaranteed if </FONT>`action'<FONT COLOR="red"> or </FONT>`test'<FONT COLOR="red"> changes the structure;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> in such a case, apply iterator to clone of structure instead.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            action_exists: action /= <B>Void</B>
            test_exits: test /= <B>Void</B>
</A>
    <A NAME="f_for_all"><A HREF="../base/linear_flatshort.html#f_for_all">for_all</A> (test: <A HREF="../base/function_flatshort.html">FUNCTION</A> [<A HREF="../base/any_flatshort.html">ANY</A>, <A HREF="../base/tuple_flatshort.html">TUPLE</A> [G], <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`test'<FONT COLOR="red"> true for all items?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Semantics not guaranteed if </FONT>`test'<FONT COLOR="red"> changes the structure;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> in such a case, apply iterator to clone of structure instead.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            test_exits: test /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
            empty: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <B>Result</B>
</A>
    <A NAME="f_there_exists"><A HREF="../base/linear_flatshort.html#f_there_exists">there_exists</A> (test: <A HREF="../base/function_flatshort.html">FUNCTION</A> [<A HREF="../base/any_flatshort.html">ANY</A>, <A HREF="../base/tuple_flatshort.html">TUPLE</A> [G], <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>]): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`test'<FONT COLOR="red"> true for at least one item?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Semantics not guaranteed if </FONT>`test'<FONT COLOR="red"> changes the structure;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> in such a case, apply iterator to clone of structure instead.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
            test_exits: test /= <B>Void</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Output</FONT>

    <A NAME="f_io"><A HREF="../base/any_flatshort.html#f_io">io</A>: <A HREF="../base/std_files_flatshort.html">STD_FILES</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Handle to standard file setup</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            io_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_out"><A HREF="../base/any_flatshort.html#f_out">out</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New string containing terse printable representation</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            out_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_print"><A HREF="../base/any_flatshort.html#f_print">print</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Write terse external representation of </FONT>`some'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> on standard output.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_tagged_out"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_tagged_out">tagged_out</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New string containing terse printable representation</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            tagged_out_not_void: <B>Result</B> /= <B>Void</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Platform</FONT>

    <A NAME="f_operating_environment"><A HREF="../base/any_flatshort.html#f_operating_environment">operating_environment</A>: <A HREF="../base/operating_environment_flatshort.html">OPERATING_ENVIRONMENT</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Objects available from the operating system</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            operating_environment_not_void: <B>Result</B> /= <B>Void</B>
</A>    
<B>invariant</B>
        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
    reflexive_equality: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (<B>Current</B>)
    reflexive_conformance: <A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (<B>Current</B>)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_struct_flatshort.html">COMPARABLE_STRUCT</A>
    empty_constraint: <A HREF="../base/comparable_struct_flatshort.html#f_min_max_available">min_max_available</A> <B>implies</B> <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bilinear_flatshort.html">BILINEAR</A>
    not_both: <B>not</B> (<A HREF="../base/linked_list_flatshort.html#f_after">after</A> <B>and</B> <A HREF="../base/linked_list_flatshort.html#f_before">before</A>)
    before_constraint: <A HREF="../base/linked_list_flatshort.html#f_before">before</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_flatshort.html">LINEAR</A>
    after_constraint: <A HREF="../base/linked_list_flatshort.html#f_after">after</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_flatshort.html">TRAVERSABLE</A>
    empty_constraint: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <A HREF="../base/linked_list_flatshort.html#f_off">off</A>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linear_subset_flatshort.html">LINEAR_SUBSET</A>
    before_definition: <A HREF="../base/linked_list_flatshort.html#f_before">before</A> = (<A HREF="../base/linked_list_flatshort.html#f_index">index</A> = 0)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/traversable_subset_flatshort.html">TRAVERSABLE_SUBSET</A>
    empty_definition: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> = (<A HREF="../base/linked_list_flatshort.html#f_count">count</A> = 0)
    count_range: <A HREF="../base/linked_list_flatshort.html#f_count">count</A> &gt;= 0

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/two_way_list_flatshort.html">TWO_WAY_LIST</A>
    non_empty_list_has_two_endpoints: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> (<A HREF="../base/two_way_list_flatshort.html#f_first_element">first_element</A> /= <B>Void</B> <B>and</B> <A HREF="../base/two_way_list_flatshort.html#f_last_element">last_element</A> /= <B>Void</B>)
    first_element_constraint: {f: <B>like</B> first_element} <A HREF="../base/two_way_list_flatshort.html#f_first_element">first_element</A> implies f.left = <B>Void</B>
    last_element_constraint: {l: <B>like</B> last_element} last_element implies l.right = <B>Void</B>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/linked_list_flatshort.html">LINKED_LIST</A>
    prunable: prunable
    empty_constraint: is_empty implies ((first_element = <B>Void</B>) and (active = <B>Void</B>))
    not_void_unless_empty: (active = <B>Void</B>) implies is_empty
    before_constraint: before implies (active = first_element)
    after_constraint: after implies (active = last_element)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/list_flatshort.html">LIST</A>
    before_definition: before = (index = 0)
    after_definition: after = (index = count + 1)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/chain_flatshort.html">CHAIN</A>
    non_negative_index: index &gt;= 0
    index_small_enough: index &lt;= count + 1
    off_definition: off = ((index = 0) or (index = count + 1))
    isfirst_definition: isfirst = ((not is_empty) and (index = 1))
    islast_definition: islast = ((not is_empty) and (index = count))
    item_corresponds_to_index: (not off) implies (item = i_th (index))
    index_set_has_same_count: index_set.count = count

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/active_flatshort.html">ACTIVE</A>
    writable_constraint: writable implies readable
    empty_constraint: is_empty implies (not readable) and (not writable)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
    index_set_not_void: index_set /= <B>Void</B>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/finite_flatshort.html">FINITE</A>
    empty_definition: is_empty = (count = 0)
    non_negative_count: count &gt;= 0

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/dynamic_chain_flatshort.html">DYNAMIC_CHAIN</A>
    extendible: extendible

<B>indexing</B>
    library: "EiffelBase: Library of reusable components for Eiffel."
    copyright: "Copyright (c) 1984-2008, Eiffel Software and others"
    license: "Eiffel Forum License v2 (see <a href="http://www.eiffel.com/licensing/forum.txt">http://www.eiffel.com/licensing/forum.txt</a>)"
    source: "[
        Eiffel Software
        356 Storke Road, Goleta, CA 93117 USA
        Telephone 805-685-1006, Fax 805-685-6869
        Website <a href="http://www.eiffel.com">http://www.eiffel.com</a>
        Customer support <a href="http://support.eiffel.com">http://support.eiffel.com</a>
    ]"

<B>end</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">class </FONT><A HREF="../base/two_way_sorted_set_flatshort.html">TWO_WAY_SORTED_SET</A><TABLE BORDER="1" ALIGN="CENTER"><TR><TD><A HREF="../class_list.html">Classes</A></TD><TD><A HREF="../cluster_list.html">Clusters</A></TD><TD><A HREF="../cluster_hierarchy.html">Cluster hierarchy</A></TD><TD><A HREF="two_way_sorted_set_chart.html">Chart</A></TD><TD><A HREF="two_way_sorted_set_links.html">Relations</A></TD><TD>Flat contracts</TD></TR></TABLE></PRE>
<P ALIGN="CENTER"> &#045;&#045; Generated by ISE Eiffel &#045;&#045 </P>
<P ALIGN="CENTER">For more details: <A HREF="http://www.eiffel.com">www.eiffel.com</A></P>
</BODY>
</HTML>

